FDL - Step of Proof: p-id-compose

Step of Proof: p-id-compose

Inference at *
Iof proof for Lemma p-id-compose:

A, B:Type, f:(A

(B + Top)). p-id() o f = f

by (Auto

)

CollapseTHEN (((Unfold `p-compose` ( 0)

)

CollapseTHEN ((Ext)

CollapseTHEN (

CReduce 0)

)

)

CollapseTHEN (((Try ((Complete (MaAuto

))

))

)

CollapseTHEN (((Try ((

CFold `p-compose` 0)

CollapseTHEN (Auto

)

))

)

CollapseTHEN (((if (0

C) =0 then SplitOnConclITE else SplitOnHypITE (0))

)

THEN (Auto

)

)

)

)

)

T1: .....truecase..... NILNIL

T1: 1. A : Type

T1: 2. B : Type

T1: 3. f : A

(B + Top)

T1: 4. x : A

T1: 5.

can-apply(f;x)

T1:

p-id()(do-apply(f;x)) = f(x)

T.

Definitions f o g , x.A(x), Unit, P Q, P & Q, x:A B(x), , x:A. B(x), P Q, if b then t else f fi , left + right, Top, f(a), p-id(), s = t, A, False, b, x:AB(x), Type, t T

Lemmas ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot